/LMAR=0/XLINE=3/FONT#3=BASB30/FONT#2=BASI30/FONT#1=BDR30/FONT#0=BDR30



␈↓ ↓H␈↓␈↓ ↓x␈↓αtransform␈↓↓[␈↓αe␈↓↓, ␈↓αr␈↓↓, ␈↓αdone␈↓↓] ←
␈↓ ↓H␈↓↓␈↓ α_␈↓βif␈↓↓ ␈↓αe␈↓↓ ε ␈↓αdone␈↓↓ ␈↓βthen␈↓↓ ␈↓αe
␈↓ ↓H␈↓α␈↓ α_␈↓βelse␈↓↓ {␈↓αtransa␈↓↓[␈↓αe␈↓↓, ␈↓αr␈↓↓]}[λ␈↓αw␈↓↓.
␈↓ ↓H␈↓↓␈↓ α8␈↓βif␈↓↓ ␈↓αw␈↓↓ ␈↓βeq ␈↓αe␈↓↓ ␈↓βthen␈↓↓
␈↓ ↓H␈↓↓␈↓ αX[␈↓βif␈↓↓ ␈↓βat ␈↓αe␈↓↓ ␈↓βthen␈↓↓ ␈↓αe
␈↓ ↓H␈↓α␈↓ αa␈↓βelse␈↓↓ {␈↓αtransform␈↓↓[␈↓βa ␈↓αe␈↓↓, ␈↓αr␈↓↓, ␈↓αdone␈↓↓], ␈↓αtransform␈↓↓[␈↓βd ␈↓αe␈↓↓, ␈↓αr␈↓↓, ␈↓αdone␈↓↓]}[λ␈↓αx␈↓↓, ␈↓αy␈↓↓.
␈↓ ↓H␈↓↓␈↓ β↓␈↓βif␈↓↓ ␈↓αx␈↓↓ ␈↓βeq a ␈↓αe␈↓↓ ∧ ␈↓αy␈↓↓ ␈↓βeq d ␈↓αe␈↓↓ ␈↓βthen␈↓↓ ␈↓αside␈↓↓[␈↓αe␈↓↓, ␈↓αdone␈↓↓ ← ␈↓αe␈↓↓ . ␈↓αdone␈↓↓] ␈↓βelse␈↓↓ ␈↓αtransform␈↓↓[␈↓αx␈↓↓ . ␈↓αy␈↓↓, ␈↓αr␈↓↓, ␈↓αdone␈↓↓]]]
␈↓ ↓H␈↓↓␈↓ α8␈↓βelse␈↓↓ ␈↓αtransform␈↓↓[␈↓αw␈↓↓, ␈↓αr␈↓↓, ␈↓αdone␈↓↓]]



␈↓ ↓H␈↓↓␈↓ ↓x␈↓αtransa␈↓↓[␈↓αe␈↓↓, ␈↓αr␈↓↓] ← ␈↓βif␈↓↓ ␈↓βn ␈↓αr␈↓↓ ␈↓βthen␈↓↓ ␈↓αe␈↓↓ ␈↓βelse␈↓↓ {␈↓αtransb␈↓↓[␈↓αe␈↓↓, ␈↓βa ␈↓αr␈↓↓]}[λ␈↓αw␈↓↓. ␈↓βif␈↓↓ ␈↓αw␈↓↓ ␈↓βeq ␈↓αe␈↓↓ ␈↓βthen␈↓↓ ␈↓αtransa␈↓↓[␈↓αe␈↓↓, ␈↓βd ␈↓αr␈↓↓] ␈↓βelse␈↓↓ ␈↓αw␈↓↓]



␈↓ ↓H␈↓↓␈↓ ↓x␈↓αtransb␈↓↓[␈↓αe␈↓↓, ␈↓αrule␈↓↓] ← {␈↓αinst␈↓↓[␈↓αe␈↓↓, ␈↓βa ␈↓αrule␈↓↓, NIL]}[λ␈↓αw␈↓↓. ␈↓βif␈↓↓ ␈↓αw␈↓↓ ␈↓βeq ␈↓↓NO ␈↓βthen␈↓↓ ␈↓αe␈↓↓ ␈↓βelse␈↓↓ ␈↓αsublis␈↓↓[␈↓βad ␈↓αrule␈↓↓, ␈↓αw␈↓↓]]



␈↓ ↓H␈↓↓␈↓ ↓x␈↓αside␈↓↓[␈↓αx␈↓↓, ␈↓αy␈↓↓] ← ␈↓αx